Nuprl Definition : rv-iid
11,40
postcript
pdf
rv-iid(
p
;
n
.
f
(
n
);
i
.
X
(
i
))
== rv-identically-distributed(
p
;
n
.
f
(
n
);
i
.
X
(
i
))
==
& (
n
:
,
i
:{0..
n
}. (
f
(
i
) <
f
(
n
)) & rv-disjoint(
p
;
f
(
n
);
X
(
i
);
X
(
n
)))
latex
Definitions
rv-identically-distributed(
p
;
n
.
f
(
n
);
i
.
X
(
i
))
,
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
#$n
,
P
&
Q
,
a
<
b
,
rv-disjoint(
p
;
n
;
X
;
Y
)
FDL editor aliases
rv-iid
origin
n:
, i:{0..n
}. (f(i) < f(n)) & rv-disjoint(p;f(n);X(i);X(n))) n:, i:{0..n}. (f(i) < f(n)) & rv-disjoint(p;f(n);X(i);X(n))) x:A. B(x)}